L:(Top List). filter(x.tt;L) ~ L 

latex

Definitions	Top, b, xL. P(x), t  T, tt, x.A(x), P  Q, x:A. B(x), type List, x:AB(x), s ~ t, (x  l), True
Lemmas	l member wf, filter trivial, btrue wf, top wf